↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
rem_in_gag(X, Y, R) → U1_gag(X, Y, R, notZero_in_a(Y))
notZero_in_a(s(X)) → notZero_out_a(s(X))
U1_gag(X, Y, R, notZero_out_a(Y)) → U2_gag(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_aaa(X, Y, Z))
sub_in_aaa(s(X), s(Y), Z) → U6_aaa(X, Y, Z, sub_in_aaa(X, Y, Z))
sub_in_aaa(X, 0, X) → sub_out_aaa(X, 0, X)
U6_aaa(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_aaa(s(X), s(Y), Z)
U6_gga(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U2_gag(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gag(X, Y, R, rem_in_agg(Z, Y, R))
rem_in_agg(X, Y, R) → U1_agg(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_agg(X, Y, R, notZero_out_g(Y)) → U2_agg(X, Y, R, sub_in_aga(X, Y, Z))
sub_in_aga(s(X), s(Y), Z) → U6_aga(X, Y, Z, sub_in_aaa(X, Y, Z))
U6_aga(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_aga(s(X), s(Y), Z)
sub_in_aga(X, 0, X) → sub_out_aga(X, 0, X)
U2_agg(X, Y, R, sub_out_aga(X, Y, Z)) → U3_agg(X, Y, R, rem_in_agg(Z, Y, R))
rem_in_agg(X, Y, X) → U4_agg(X, Y, notZero_in_g(Y))
U4_agg(X, Y, notZero_out_g(Y)) → U5_agg(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_aa(X, Y))
geq_in_aa(s(X), s(Y)) → U7_aa(X, Y, geq_in_aa(X, Y))
geq_in_aa(X, 0) → geq_out_aa(X, 0)
U7_aa(X, Y, geq_out_aa(X, Y)) → geq_out_aa(s(X), s(Y))
U7_gg(X, Y, geq_out_aa(X, Y)) → geq_out_gg(s(X), s(Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U5_agg(X, Y, geq_out_gg(X, Y)) → rem_out_agg(X, Y, X)
U3_agg(X, Y, R, rem_out_agg(Z, Y, R)) → rem_out_agg(X, Y, R)
U3_gag(X, Y, R, rem_out_agg(Z, Y, R)) → rem_out_gag(X, Y, R)
rem_in_gag(X, Y, X) → U4_gag(X, Y, notZero_in_a(Y))
U4_gag(X, Y, notZero_out_a(Y)) → U5_gag(X, Y, geq_in_gg(X, Y))
U5_gag(X, Y, geq_out_gg(X, Y)) → rem_out_gag(X, Y, X)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PrologToPiTRSProof
rem_in_gag(X, Y, R) → U1_gag(X, Y, R, notZero_in_a(Y))
notZero_in_a(s(X)) → notZero_out_a(s(X))
U1_gag(X, Y, R, notZero_out_a(Y)) → U2_gag(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_aaa(X, Y, Z))
sub_in_aaa(s(X), s(Y), Z) → U6_aaa(X, Y, Z, sub_in_aaa(X, Y, Z))
sub_in_aaa(X, 0, X) → sub_out_aaa(X, 0, X)
U6_aaa(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_aaa(s(X), s(Y), Z)
U6_gga(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U2_gag(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gag(X, Y, R, rem_in_agg(Z, Y, R))
rem_in_agg(X, Y, R) → U1_agg(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_agg(X, Y, R, notZero_out_g(Y)) → U2_agg(X, Y, R, sub_in_aga(X, Y, Z))
sub_in_aga(s(X), s(Y), Z) → U6_aga(X, Y, Z, sub_in_aaa(X, Y, Z))
U6_aga(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_aga(s(X), s(Y), Z)
sub_in_aga(X, 0, X) → sub_out_aga(X, 0, X)
U2_agg(X, Y, R, sub_out_aga(X, Y, Z)) → U3_agg(X, Y, R, rem_in_agg(Z, Y, R))
rem_in_agg(X, Y, X) → U4_agg(X, Y, notZero_in_g(Y))
U4_agg(X, Y, notZero_out_g(Y)) → U5_agg(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_aa(X, Y))
geq_in_aa(s(X), s(Y)) → U7_aa(X, Y, geq_in_aa(X, Y))
geq_in_aa(X, 0) → geq_out_aa(X, 0)
U7_aa(X, Y, geq_out_aa(X, Y)) → geq_out_aa(s(X), s(Y))
U7_gg(X, Y, geq_out_aa(X, Y)) → geq_out_gg(s(X), s(Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U5_agg(X, Y, geq_out_gg(X, Y)) → rem_out_agg(X, Y, X)
U3_agg(X, Y, R, rem_out_agg(Z, Y, R)) → rem_out_agg(X, Y, R)
U3_gag(X, Y, R, rem_out_agg(Z, Y, R)) → rem_out_gag(X, Y, R)
rem_in_gag(X, Y, X) → U4_gag(X, Y, notZero_in_a(Y))
U4_gag(X, Y, notZero_out_a(Y)) → U5_gag(X, Y, geq_in_gg(X, Y))
U5_gag(X, Y, geq_out_gg(X, Y)) → rem_out_gag(X, Y, X)
REM_IN_GAG(X, Y, R) → U1_GAG(X, Y, R, notZero_in_a(Y))
REM_IN_GAG(X, Y, R) → NOTZERO_IN_A(Y)
U1_GAG(X, Y, R, notZero_out_a(Y)) → U2_GAG(X, Y, R, sub_in_gga(X, Y, Z))
U1_GAG(X, Y, R, notZero_out_a(Y)) → SUB_IN_GGA(X, Y, Z)
SUB_IN_GGA(s(X), s(Y), Z) → U6_GGA(X, Y, Z, sub_in_aaa(X, Y, Z))
SUB_IN_GGA(s(X), s(Y), Z) → SUB_IN_AAA(X, Y, Z)
SUB_IN_AAA(s(X), s(Y), Z) → U6_AAA(X, Y, Z, sub_in_aaa(X, Y, Z))
SUB_IN_AAA(s(X), s(Y), Z) → SUB_IN_AAA(X, Y, Z)
U2_GAG(X, Y, R, sub_out_gga(X, Y, Z)) → U3_GAG(X, Y, R, rem_in_agg(Z, Y, R))
U2_GAG(X, Y, R, sub_out_gga(X, Y, Z)) → REM_IN_AGG(Z, Y, R)
REM_IN_AGG(X, Y, R) → U1_AGG(X, Y, R, notZero_in_g(Y))
REM_IN_AGG(X, Y, R) → NOTZERO_IN_G(Y)
U1_AGG(X, Y, R, notZero_out_g(Y)) → U2_AGG(X, Y, R, sub_in_aga(X, Y, Z))
U1_AGG(X, Y, R, notZero_out_g(Y)) → SUB_IN_AGA(X, Y, Z)
SUB_IN_AGA(s(X), s(Y), Z) → U6_AGA(X, Y, Z, sub_in_aaa(X, Y, Z))
SUB_IN_AGA(s(X), s(Y), Z) → SUB_IN_AAA(X, Y, Z)
U2_AGG(X, Y, R, sub_out_aga(X, Y, Z)) → U3_AGG(X, Y, R, rem_in_agg(Z, Y, R))
U2_AGG(X, Y, R, sub_out_aga(X, Y, Z)) → REM_IN_AGG(Z, Y, R)
REM_IN_AGG(X, Y, X) → U4_AGG(X, Y, notZero_in_g(Y))
REM_IN_AGG(X, Y, X) → NOTZERO_IN_G(Y)
U4_AGG(X, Y, notZero_out_g(Y)) → U5_AGG(X, Y, geq_in_gg(X, Y))
U4_AGG(X, Y, notZero_out_g(Y)) → GEQ_IN_GG(X, Y)
GEQ_IN_GG(s(X), s(Y)) → U7_GG(X, Y, geq_in_aa(X, Y))
GEQ_IN_GG(s(X), s(Y)) → GEQ_IN_AA(X, Y)
GEQ_IN_AA(s(X), s(Y)) → U7_AA(X, Y, geq_in_aa(X, Y))
GEQ_IN_AA(s(X), s(Y)) → GEQ_IN_AA(X, Y)
REM_IN_GAG(X, Y, X) → U4_GAG(X, Y, notZero_in_a(Y))
REM_IN_GAG(X, Y, X) → NOTZERO_IN_A(Y)
U4_GAG(X, Y, notZero_out_a(Y)) → U5_GAG(X, Y, geq_in_gg(X, Y))
U4_GAG(X, Y, notZero_out_a(Y)) → GEQ_IN_GG(X, Y)
rem_in_gag(X, Y, R) → U1_gag(X, Y, R, notZero_in_a(Y))
notZero_in_a(s(X)) → notZero_out_a(s(X))
U1_gag(X, Y, R, notZero_out_a(Y)) → U2_gag(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_aaa(X, Y, Z))
sub_in_aaa(s(X), s(Y), Z) → U6_aaa(X, Y, Z, sub_in_aaa(X, Y, Z))
sub_in_aaa(X, 0, X) → sub_out_aaa(X, 0, X)
U6_aaa(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_aaa(s(X), s(Y), Z)
U6_gga(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U2_gag(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gag(X, Y, R, rem_in_agg(Z, Y, R))
rem_in_agg(X, Y, R) → U1_agg(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_agg(X, Y, R, notZero_out_g(Y)) → U2_agg(X, Y, R, sub_in_aga(X, Y, Z))
sub_in_aga(s(X), s(Y), Z) → U6_aga(X, Y, Z, sub_in_aaa(X, Y, Z))
U6_aga(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_aga(s(X), s(Y), Z)
sub_in_aga(X, 0, X) → sub_out_aga(X, 0, X)
U2_agg(X, Y, R, sub_out_aga(X, Y, Z)) → U3_agg(X, Y, R, rem_in_agg(Z, Y, R))
rem_in_agg(X, Y, X) → U4_agg(X, Y, notZero_in_g(Y))
U4_agg(X, Y, notZero_out_g(Y)) → U5_agg(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_aa(X, Y))
geq_in_aa(s(X), s(Y)) → U7_aa(X, Y, geq_in_aa(X, Y))
geq_in_aa(X, 0) → geq_out_aa(X, 0)
U7_aa(X, Y, geq_out_aa(X, Y)) → geq_out_aa(s(X), s(Y))
U7_gg(X, Y, geq_out_aa(X, Y)) → geq_out_gg(s(X), s(Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U5_agg(X, Y, geq_out_gg(X, Y)) → rem_out_agg(X, Y, X)
U3_agg(X, Y, R, rem_out_agg(Z, Y, R)) → rem_out_agg(X, Y, R)
U3_gag(X, Y, R, rem_out_agg(Z, Y, R)) → rem_out_gag(X, Y, R)
rem_in_gag(X, Y, X) → U4_gag(X, Y, notZero_in_a(Y))
U4_gag(X, Y, notZero_out_a(Y)) → U5_gag(X, Y, geq_in_gg(X, Y))
U5_gag(X, Y, geq_out_gg(X, Y)) → rem_out_gag(X, Y, X)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PrologToPiTRSProof
REM_IN_GAG(X, Y, R) → U1_GAG(X, Y, R, notZero_in_a(Y))
REM_IN_GAG(X, Y, R) → NOTZERO_IN_A(Y)
U1_GAG(X, Y, R, notZero_out_a(Y)) → U2_GAG(X, Y, R, sub_in_gga(X, Y, Z))
U1_GAG(X, Y, R, notZero_out_a(Y)) → SUB_IN_GGA(X, Y, Z)
SUB_IN_GGA(s(X), s(Y), Z) → U6_GGA(X, Y, Z, sub_in_aaa(X, Y, Z))
SUB_IN_GGA(s(X), s(Y), Z) → SUB_IN_AAA(X, Y, Z)
SUB_IN_AAA(s(X), s(Y), Z) → U6_AAA(X, Y, Z, sub_in_aaa(X, Y, Z))
SUB_IN_AAA(s(X), s(Y), Z) → SUB_IN_AAA(X, Y, Z)
U2_GAG(X, Y, R, sub_out_gga(X, Y, Z)) → U3_GAG(X, Y, R, rem_in_agg(Z, Y, R))
U2_GAG(X, Y, R, sub_out_gga(X, Y, Z)) → REM_IN_AGG(Z, Y, R)
REM_IN_AGG(X, Y, R) → U1_AGG(X, Y, R, notZero_in_g(Y))
REM_IN_AGG(X, Y, R) → NOTZERO_IN_G(Y)
U1_AGG(X, Y, R, notZero_out_g(Y)) → U2_AGG(X, Y, R, sub_in_aga(X, Y, Z))
U1_AGG(X, Y, R, notZero_out_g(Y)) → SUB_IN_AGA(X, Y, Z)
SUB_IN_AGA(s(X), s(Y), Z) → U6_AGA(X, Y, Z, sub_in_aaa(X, Y, Z))
SUB_IN_AGA(s(X), s(Y), Z) → SUB_IN_AAA(X, Y, Z)
U2_AGG(X, Y, R, sub_out_aga(X, Y, Z)) → U3_AGG(X, Y, R, rem_in_agg(Z, Y, R))
U2_AGG(X, Y, R, sub_out_aga(X, Y, Z)) → REM_IN_AGG(Z, Y, R)
REM_IN_AGG(X, Y, X) → U4_AGG(X, Y, notZero_in_g(Y))
REM_IN_AGG(X, Y, X) → NOTZERO_IN_G(Y)
U4_AGG(X, Y, notZero_out_g(Y)) → U5_AGG(X, Y, geq_in_gg(X, Y))
U4_AGG(X, Y, notZero_out_g(Y)) → GEQ_IN_GG(X, Y)
GEQ_IN_GG(s(X), s(Y)) → U7_GG(X, Y, geq_in_aa(X, Y))
GEQ_IN_GG(s(X), s(Y)) → GEQ_IN_AA(X, Y)
GEQ_IN_AA(s(X), s(Y)) → U7_AA(X, Y, geq_in_aa(X, Y))
GEQ_IN_AA(s(X), s(Y)) → GEQ_IN_AA(X, Y)
REM_IN_GAG(X, Y, X) → U4_GAG(X, Y, notZero_in_a(Y))
REM_IN_GAG(X, Y, X) → NOTZERO_IN_A(Y)
U4_GAG(X, Y, notZero_out_a(Y)) → U5_GAG(X, Y, geq_in_gg(X, Y))
U4_GAG(X, Y, notZero_out_a(Y)) → GEQ_IN_GG(X, Y)
rem_in_gag(X, Y, R) → U1_gag(X, Y, R, notZero_in_a(Y))
notZero_in_a(s(X)) → notZero_out_a(s(X))
U1_gag(X, Y, R, notZero_out_a(Y)) → U2_gag(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_aaa(X, Y, Z))
sub_in_aaa(s(X), s(Y), Z) → U6_aaa(X, Y, Z, sub_in_aaa(X, Y, Z))
sub_in_aaa(X, 0, X) → sub_out_aaa(X, 0, X)
U6_aaa(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_aaa(s(X), s(Y), Z)
U6_gga(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U2_gag(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gag(X, Y, R, rem_in_agg(Z, Y, R))
rem_in_agg(X, Y, R) → U1_agg(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_agg(X, Y, R, notZero_out_g(Y)) → U2_agg(X, Y, R, sub_in_aga(X, Y, Z))
sub_in_aga(s(X), s(Y), Z) → U6_aga(X, Y, Z, sub_in_aaa(X, Y, Z))
U6_aga(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_aga(s(X), s(Y), Z)
sub_in_aga(X, 0, X) → sub_out_aga(X, 0, X)
U2_agg(X, Y, R, sub_out_aga(X, Y, Z)) → U3_agg(X, Y, R, rem_in_agg(Z, Y, R))
rem_in_agg(X, Y, X) → U4_agg(X, Y, notZero_in_g(Y))
U4_agg(X, Y, notZero_out_g(Y)) → U5_agg(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_aa(X, Y))
geq_in_aa(s(X), s(Y)) → U7_aa(X, Y, geq_in_aa(X, Y))
geq_in_aa(X, 0) → geq_out_aa(X, 0)
U7_aa(X, Y, geq_out_aa(X, Y)) → geq_out_aa(s(X), s(Y))
U7_gg(X, Y, geq_out_aa(X, Y)) → geq_out_gg(s(X), s(Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U5_agg(X, Y, geq_out_gg(X, Y)) → rem_out_agg(X, Y, X)
U3_agg(X, Y, R, rem_out_agg(Z, Y, R)) → rem_out_agg(X, Y, R)
U3_gag(X, Y, R, rem_out_agg(Z, Y, R)) → rem_out_gag(X, Y, R)
rem_in_gag(X, Y, X) → U4_gag(X, Y, notZero_in_a(Y))
U4_gag(X, Y, notZero_out_a(Y)) → U5_gag(X, Y, geq_in_gg(X, Y))
U5_gag(X, Y, geq_out_gg(X, Y)) → rem_out_gag(X, Y, X)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDP
↳ PrologToPiTRSProof
GEQ_IN_AA(s(X), s(Y)) → GEQ_IN_AA(X, Y)
rem_in_gag(X, Y, R) → U1_gag(X, Y, R, notZero_in_a(Y))
notZero_in_a(s(X)) → notZero_out_a(s(X))
U1_gag(X, Y, R, notZero_out_a(Y)) → U2_gag(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_aaa(X, Y, Z))
sub_in_aaa(s(X), s(Y), Z) → U6_aaa(X, Y, Z, sub_in_aaa(X, Y, Z))
sub_in_aaa(X, 0, X) → sub_out_aaa(X, 0, X)
U6_aaa(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_aaa(s(X), s(Y), Z)
U6_gga(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U2_gag(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gag(X, Y, R, rem_in_agg(Z, Y, R))
rem_in_agg(X, Y, R) → U1_agg(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_agg(X, Y, R, notZero_out_g(Y)) → U2_agg(X, Y, R, sub_in_aga(X, Y, Z))
sub_in_aga(s(X), s(Y), Z) → U6_aga(X, Y, Z, sub_in_aaa(X, Y, Z))
U6_aga(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_aga(s(X), s(Y), Z)
sub_in_aga(X, 0, X) → sub_out_aga(X, 0, X)
U2_agg(X, Y, R, sub_out_aga(X, Y, Z)) → U3_agg(X, Y, R, rem_in_agg(Z, Y, R))
rem_in_agg(X, Y, X) → U4_agg(X, Y, notZero_in_g(Y))
U4_agg(X, Y, notZero_out_g(Y)) → U5_agg(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_aa(X, Y))
geq_in_aa(s(X), s(Y)) → U7_aa(X, Y, geq_in_aa(X, Y))
geq_in_aa(X, 0) → geq_out_aa(X, 0)
U7_aa(X, Y, geq_out_aa(X, Y)) → geq_out_aa(s(X), s(Y))
U7_gg(X, Y, geq_out_aa(X, Y)) → geq_out_gg(s(X), s(Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U5_agg(X, Y, geq_out_gg(X, Y)) → rem_out_agg(X, Y, X)
U3_agg(X, Y, R, rem_out_agg(Z, Y, R)) → rem_out_agg(X, Y, R)
U3_gag(X, Y, R, rem_out_agg(Z, Y, R)) → rem_out_gag(X, Y, R)
rem_in_gag(X, Y, X) → U4_gag(X, Y, notZero_in_a(Y))
U4_gag(X, Y, notZero_out_a(Y)) → U5_gag(X, Y, geq_in_gg(X, Y))
U5_gag(X, Y, geq_out_gg(X, Y)) → rem_out_gag(X, Y, X)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PiDP
↳ PrologToPiTRSProof
GEQ_IN_AA(s(X), s(Y)) → GEQ_IN_AA(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ NonTerminationProof
↳ PiDP
↳ PiDP
↳ PrologToPiTRSProof
GEQ_IN_AA → GEQ_IN_AA
GEQ_IN_AA → GEQ_IN_AA
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PrologToPiTRSProof
SUB_IN_AAA(s(X), s(Y), Z) → SUB_IN_AAA(X, Y, Z)
rem_in_gag(X, Y, R) → U1_gag(X, Y, R, notZero_in_a(Y))
notZero_in_a(s(X)) → notZero_out_a(s(X))
U1_gag(X, Y, R, notZero_out_a(Y)) → U2_gag(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_aaa(X, Y, Z))
sub_in_aaa(s(X), s(Y), Z) → U6_aaa(X, Y, Z, sub_in_aaa(X, Y, Z))
sub_in_aaa(X, 0, X) → sub_out_aaa(X, 0, X)
U6_aaa(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_aaa(s(X), s(Y), Z)
U6_gga(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U2_gag(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gag(X, Y, R, rem_in_agg(Z, Y, R))
rem_in_agg(X, Y, R) → U1_agg(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_agg(X, Y, R, notZero_out_g(Y)) → U2_agg(X, Y, R, sub_in_aga(X, Y, Z))
sub_in_aga(s(X), s(Y), Z) → U6_aga(X, Y, Z, sub_in_aaa(X, Y, Z))
U6_aga(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_aga(s(X), s(Y), Z)
sub_in_aga(X, 0, X) → sub_out_aga(X, 0, X)
U2_agg(X, Y, R, sub_out_aga(X, Y, Z)) → U3_agg(X, Y, R, rem_in_agg(Z, Y, R))
rem_in_agg(X, Y, X) → U4_agg(X, Y, notZero_in_g(Y))
U4_agg(X, Y, notZero_out_g(Y)) → U5_agg(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_aa(X, Y))
geq_in_aa(s(X), s(Y)) → U7_aa(X, Y, geq_in_aa(X, Y))
geq_in_aa(X, 0) → geq_out_aa(X, 0)
U7_aa(X, Y, geq_out_aa(X, Y)) → geq_out_aa(s(X), s(Y))
U7_gg(X, Y, geq_out_aa(X, Y)) → geq_out_gg(s(X), s(Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U5_agg(X, Y, geq_out_gg(X, Y)) → rem_out_agg(X, Y, X)
U3_agg(X, Y, R, rem_out_agg(Z, Y, R)) → rem_out_agg(X, Y, R)
U3_gag(X, Y, R, rem_out_agg(Z, Y, R)) → rem_out_gag(X, Y, R)
rem_in_gag(X, Y, X) → U4_gag(X, Y, notZero_in_a(Y))
U4_gag(X, Y, notZero_out_a(Y)) → U5_gag(X, Y, geq_in_gg(X, Y))
U5_gag(X, Y, geq_out_gg(X, Y)) → rem_out_gag(X, Y, X)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PrologToPiTRSProof
SUB_IN_AAA(s(X), s(Y), Z) → SUB_IN_AAA(X, Y, Z)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ NonTerminationProof
↳ PiDP
↳ PrologToPiTRSProof
SUB_IN_AAA → SUB_IN_AAA
SUB_IN_AAA → SUB_IN_AAA
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PrologToPiTRSProof
U1_AGG(X, Y, R, notZero_out_g(Y)) → U2_AGG(X, Y, R, sub_in_aga(X, Y, Z))
U2_AGG(X, Y, R, sub_out_aga(X, Y, Z)) → REM_IN_AGG(Z, Y, R)
REM_IN_AGG(X, Y, R) → U1_AGG(X, Y, R, notZero_in_g(Y))
rem_in_gag(X, Y, R) → U1_gag(X, Y, R, notZero_in_a(Y))
notZero_in_a(s(X)) → notZero_out_a(s(X))
U1_gag(X, Y, R, notZero_out_a(Y)) → U2_gag(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_aaa(X, Y, Z))
sub_in_aaa(s(X), s(Y), Z) → U6_aaa(X, Y, Z, sub_in_aaa(X, Y, Z))
sub_in_aaa(X, 0, X) → sub_out_aaa(X, 0, X)
U6_aaa(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_aaa(s(X), s(Y), Z)
U6_gga(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U2_gag(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gag(X, Y, R, rem_in_agg(Z, Y, R))
rem_in_agg(X, Y, R) → U1_agg(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_agg(X, Y, R, notZero_out_g(Y)) → U2_agg(X, Y, R, sub_in_aga(X, Y, Z))
sub_in_aga(s(X), s(Y), Z) → U6_aga(X, Y, Z, sub_in_aaa(X, Y, Z))
U6_aga(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_aga(s(X), s(Y), Z)
sub_in_aga(X, 0, X) → sub_out_aga(X, 0, X)
U2_agg(X, Y, R, sub_out_aga(X, Y, Z)) → U3_agg(X, Y, R, rem_in_agg(Z, Y, R))
rem_in_agg(X, Y, X) → U4_agg(X, Y, notZero_in_g(Y))
U4_agg(X, Y, notZero_out_g(Y)) → U5_agg(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_aa(X, Y))
geq_in_aa(s(X), s(Y)) → U7_aa(X, Y, geq_in_aa(X, Y))
geq_in_aa(X, 0) → geq_out_aa(X, 0)
U7_aa(X, Y, geq_out_aa(X, Y)) → geq_out_aa(s(X), s(Y))
U7_gg(X, Y, geq_out_aa(X, Y)) → geq_out_gg(s(X), s(Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U5_agg(X, Y, geq_out_gg(X, Y)) → rem_out_agg(X, Y, X)
U3_agg(X, Y, R, rem_out_agg(Z, Y, R)) → rem_out_agg(X, Y, R)
U3_gag(X, Y, R, rem_out_agg(Z, Y, R)) → rem_out_gag(X, Y, R)
rem_in_gag(X, Y, X) → U4_gag(X, Y, notZero_in_a(Y))
U4_gag(X, Y, notZero_out_a(Y)) → U5_gag(X, Y, geq_in_gg(X, Y))
U5_gag(X, Y, geq_out_gg(X, Y)) → rem_out_gag(X, Y, X)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PrologToPiTRSProof
U1_AGG(X, Y, R, notZero_out_g(Y)) → U2_AGG(X, Y, R, sub_in_aga(X, Y, Z))
U2_AGG(X, Y, R, sub_out_aga(X, Y, Z)) → REM_IN_AGG(Z, Y, R)
REM_IN_AGG(X, Y, R) → U1_AGG(X, Y, R, notZero_in_g(Y))
sub_in_aga(s(X), s(Y), Z) → U6_aga(X, Y, Z, sub_in_aaa(X, Y, Z))
sub_in_aga(X, 0, X) → sub_out_aga(X, 0, X)
notZero_in_g(s(X)) → notZero_out_g(s(X))
U6_aga(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_aga(s(X), s(Y), Z)
sub_in_aaa(s(X), s(Y), Z) → U6_aaa(X, Y, Z, sub_in_aaa(X, Y, Z))
sub_in_aaa(X, 0, X) → sub_out_aaa(X, 0, X)
U6_aaa(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_aaa(s(X), s(Y), Z)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ PrologToPiTRSProof
U1_AGG(Y, R, notZero_out_g) → U2_AGG(Y, R, sub_in_aga(Y))
REM_IN_AGG(Y, R) → U1_AGG(Y, R, notZero_in_g(Y))
U2_AGG(Y, R, sub_out_aga) → REM_IN_AGG(Y, R)
sub_in_aga(s) → U6_aga(sub_in_aaa)
sub_in_aga(0) → sub_out_aga
notZero_in_g(s) → notZero_out_g
U6_aga(sub_out_aaa(Y)) → sub_out_aga
sub_in_aaa → U6_aaa(sub_in_aaa)
sub_in_aaa → sub_out_aaa(0)
U6_aaa(sub_out_aaa(Y)) → sub_out_aaa(s)
sub_in_aga(x0)
notZero_in_g(x0)
U6_aga(x0)
sub_in_aaa
U6_aaa(x0)
U1_AGG(0, y1, notZero_out_g) → U2_AGG(0, y1, sub_out_aga)
U1_AGG(s, y1, notZero_out_g) → U2_AGG(s, y1, U6_aga(sub_in_aaa))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ PrologToPiTRSProof
U1_AGG(0, y1, notZero_out_g) → U2_AGG(0, y1, sub_out_aga)
REM_IN_AGG(Y, R) → U1_AGG(Y, R, notZero_in_g(Y))
U1_AGG(s, y1, notZero_out_g) → U2_AGG(s, y1, U6_aga(sub_in_aaa))
U2_AGG(Y, R, sub_out_aga) → REM_IN_AGG(Y, R)
sub_in_aga(s) → U6_aga(sub_in_aaa)
sub_in_aga(0) → sub_out_aga
notZero_in_g(s) → notZero_out_g
U6_aga(sub_out_aaa(Y)) → sub_out_aga
sub_in_aaa → U6_aaa(sub_in_aaa)
sub_in_aaa → sub_out_aaa(0)
U6_aaa(sub_out_aaa(Y)) → sub_out_aaa(s)
sub_in_aga(x0)
notZero_in_g(x0)
U6_aga(x0)
sub_in_aaa
U6_aaa(x0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ PrologToPiTRSProof
U1_AGG(0, y1, notZero_out_g) → U2_AGG(0, y1, sub_out_aga)
REM_IN_AGG(Y, R) → U1_AGG(Y, R, notZero_in_g(Y))
U1_AGG(s, y1, notZero_out_g) → U2_AGG(s, y1, U6_aga(sub_in_aaa))
U2_AGG(Y, R, sub_out_aga) → REM_IN_AGG(Y, R)
sub_in_aaa → U6_aaa(sub_in_aaa)
sub_in_aaa → sub_out_aaa(0)
U6_aga(sub_out_aaa(Y)) → sub_out_aga
U6_aaa(sub_out_aaa(Y)) → sub_out_aaa(s)
notZero_in_g(s) → notZero_out_g
sub_in_aga(x0)
notZero_in_g(x0)
U6_aga(x0)
sub_in_aaa
U6_aaa(x0)
sub_in_aga(x0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ PrologToPiTRSProof
U1_AGG(0, y1, notZero_out_g) → U2_AGG(0, y1, sub_out_aga)
REM_IN_AGG(Y, R) → U1_AGG(Y, R, notZero_in_g(Y))
U1_AGG(s, y1, notZero_out_g) → U2_AGG(s, y1, U6_aga(sub_in_aaa))
U2_AGG(Y, R, sub_out_aga) → REM_IN_AGG(Y, R)
sub_in_aaa → U6_aaa(sub_in_aaa)
sub_in_aaa → sub_out_aaa(0)
U6_aga(sub_out_aaa(Y)) → sub_out_aga
U6_aaa(sub_out_aaa(Y)) → sub_out_aaa(s)
notZero_in_g(s) → notZero_out_g
notZero_in_g(x0)
U6_aga(x0)
sub_in_aaa
U6_aaa(x0)
REM_IN_AGG(s, y1) → U1_AGG(s, y1, notZero_out_g)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ PrologToPiTRSProof
U1_AGG(0, y1, notZero_out_g) → U2_AGG(0, y1, sub_out_aga)
REM_IN_AGG(s, y1) → U1_AGG(s, y1, notZero_out_g)
U1_AGG(s, y1, notZero_out_g) → U2_AGG(s, y1, U6_aga(sub_in_aaa))
U2_AGG(Y, R, sub_out_aga) → REM_IN_AGG(Y, R)
sub_in_aaa → U6_aaa(sub_in_aaa)
sub_in_aaa → sub_out_aaa(0)
U6_aga(sub_out_aaa(Y)) → sub_out_aga
U6_aaa(sub_out_aaa(Y)) → sub_out_aaa(s)
notZero_in_g(s) → notZero_out_g
notZero_in_g(x0)
U6_aga(x0)
sub_in_aaa
U6_aaa(x0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ PrologToPiTRSProof
REM_IN_AGG(s, y1) → U1_AGG(s, y1, notZero_out_g)
U1_AGG(s, y1, notZero_out_g) → U2_AGG(s, y1, U6_aga(sub_in_aaa))
U2_AGG(Y, R, sub_out_aga) → REM_IN_AGG(Y, R)
sub_in_aaa → U6_aaa(sub_in_aaa)
sub_in_aaa → sub_out_aaa(0)
U6_aga(sub_out_aaa(Y)) → sub_out_aga
U6_aaa(sub_out_aaa(Y)) → sub_out_aaa(s)
notZero_in_g(s) → notZero_out_g
notZero_in_g(x0)
U6_aga(x0)
sub_in_aaa
U6_aaa(x0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ PrologToPiTRSProof
REM_IN_AGG(s, y1) → U1_AGG(s, y1, notZero_out_g)
U1_AGG(s, y1, notZero_out_g) → U2_AGG(s, y1, U6_aga(sub_in_aaa))
U2_AGG(Y, R, sub_out_aga) → REM_IN_AGG(Y, R)
sub_in_aaa → U6_aaa(sub_in_aaa)
sub_in_aaa → sub_out_aaa(0)
U6_aga(sub_out_aaa(Y)) → sub_out_aga
U6_aaa(sub_out_aaa(Y)) → sub_out_aaa(s)
notZero_in_g(x0)
U6_aga(x0)
sub_in_aaa
U6_aaa(x0)
notZero_in_g(x0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ PrologToPiTRSProof
REM_IN_AGG(s, y1) → U1_AGG(s, y1, notZero_out_g)
U1_AGG(s, y1, notZero_out_g) → U2_AGG(s, y1, U6_aga(sub_in_aaa))
U2_AGG(Y, R, sub_out_aga) → REM_IN_AGG(Y, R)
sub_in_aaa → U6_aaa(sub_in_aaa)
sub_in_aaa → sub_out_aaa(0)
U6_aga(sub_out_aaa(Y)) → sub_out_aga
U6_aaa(sub_out_aaa(Y)) → sub_out_aaa(s)
U6_aga(x0)
sub_in_aaa
U6_aaa(x0)
U2_AGG(s, z0, sub_out_aga) → REM_IN_AGG(s, z0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ NonTerminationProof
↳ PrologToPiTRSProof
U2_AGG(s, z0, sub_out_aga) → REM_IN_AGG(s, z0)
REM_IN_AGG(s, y1) → U1_AGG(s, y1, notZero_out_g)
U1_AGG(s, y1, notZero_out_g) → U2_AGG(s, y1, U6_aga(sub_in_aaa))
sub_in_aaa → U6_aaa(sub_in_aaa)
sub_in_aaa → sub_out_aaa(0)
U6_aga(sub_out_aaa(Y)) → sub_out_aga
U6_aaa(sub_out_aaa(Y)) → sub_out_aaa(s)
U6_aga(x0)
sub_in_aaa
U6_aaa(x0)
U2_AGG(s, z0, sub_out_aga) → REM_IN_AGG(s, z0)
REM_IN_AGG(s, y1) → U1_AGG(s, y1, notZero_out_g)
U1_AGG(s, y1, notZero_out_g) → U2_AGG(s, y1, U6_aga(sub_in_aaa))
sub_in_aaa → U6_aaa(sub_in_aaa)
sub_in_aaa → sub_out_aaa(0)
U6_aga(sub_out_aaa(Y)) → sub_out_aga
U6_aaa(sub_out_aaa(Y)) → sub_out_aaa(s)
rem_in_gag(X, Y, R) → U1_gag(X, Y, R, notZero_in_a(Y))
notZero_in_a(s(X)) → notZero_out_a(s(X))
U1_gag(X, Y, R, notZero_out_a(Y)) → U2_gag(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_aaa(X, Y, Z))
sub_in_aaa(s(X), s(Y), Z) → U6_aaa(X, Y, Z, sub_in_aaa(X, Y, Z))
sub_in_aaa(X, 0, X) → sub_out_aaa(X, 0, X)
U6_aaa(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_aaa(s(X), s(Y), Z)
U6_gga(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U2_gag(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gag(X, Y, R, rem_in_agg(Z, Y, R))
rem_in_agg(X, Y, R) → U1_agg(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_agg(X, Y, R, notZero_out_g(Y)) → U2_agg(X, Y, R, sub_in_aga(X, Y, Z))
sub_in_aga(s(X), s(Y), Z) → U6_aga(X, Y, Z, sub_in_aaa(X, Y, Z))
U6_aga(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_aga(s(X), s(Y), Z)
sub_in_aga(X, 0, X) → sub_out_aga(X, 0, X)
U2_agg(X, Y, R, sub_out_aga(X, Y, Z)) → U3_agg(X, Y, R, rem_in_agg(Z, Y, R))
rem_in_agg(X, Y, X) → U4_agg(X, Y, notZero_in_g(Y))
U4_agg(X, Y, notZero_out_g(Y)) → U5_agg(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_aa(X, Y))
geq_in_aa(s(X), s(Y)) → U7_aa(X, Y, geq_in_aa(X, Y))
geq_in_aa(X, 0) → geq_out_aa(X, 0)
U7_aa(X, Y, geq_out_aa(X, Y)) → geq_out_aa(s(X), s(Y))
U7_gg(X, Y, geq_out_aa(X, Y)) → geq_out_gg(s(X), s(Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U5_agg(X, Y, geq_out_gg(X, Y)) → rem_out_agg(X, Y, X)
U3_agg(X, Y, R, rem_out_agg(Z, Y, R)) → rem_out_agg(X, Y, R)
U3_gag(X, Y, R, rem_out_agg(Z, Y, R)) → rem_out_gag(X, Y, R)
rem_in_gag(X, Y, X) → U4_gag(X, Y, notZero_in_a(Y))
U4_gag(X, Y, notZero_out_a(Y)) → U5_gag(X, Y, geq_in_gg(X, Y))
U5_gag(X, Y, geq_out_gg(X, Y)) → rem_out_gag(X, Y, X)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
rem_in_gag(X, Y, R) → U1_gag(X, Y, R, notZero_in_a(Y))
notZero_in_a(s(X)) → notZero_out_a(s(X))
U1_gag(X, Y, R, notZero_out_a(Y)) → U2_gag(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_aaa(X, Y, Z))
sub_in_aaa(s(X), s(Y), Z) → U6_aaa(X, Y, Z, sub_in_aaa(X, Y, Z))
sub_in_aaa(X, 0, X) → sub_out_aaa(X, 0, X)
U6_aaa(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_aaa(s(X), s(Y), Z)
U6_gga(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U2_gag(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gag(X, Y, R, rem_in_agg(Z, Y, R))
rem_in_agg(X, Y, R) → U1_agg(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_agg(X, Y, R, notZero_out_g(Y)) → U2_agg(X, Y, R, sub_in_aga(X, Y, Z))
sub_in_aga(s(X), s(Y), Z) → U6_aga(X, Y, Z, sub_in_aaa(X, Y, Z))
U6_aga(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_aga(s(X), s(Y), Z)
sub_in_aga(X, 0, X) → sub_out_aga(X, 0, X)
U2_agg(X, Y, R, sub_out_aga(X, Y, Z)) → U3_agg(X, Y, R, rem_in_agg(Z, Y, R))
rem_in_agg(X, Y, X) → U4_agg(X, Y, notZero_in_g(Y))
U4_agg(X, Y, notZero_out_g(Y)) → U5_agg(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_aa(X, Y))
geq_in_aa(s(X), s(Y)) → U7_aa(X, Y, geq_in_aa(X, Y))
geq_in_aa(X, 0) → geq_out_aa(X, 0)
U7_aa(X, Y, geq_out_aa(X, Y)) → geq_out_aa(s(X), s(Y))
U7_gg(X, Y, geq_out_aa(X, Y)) → geq_out_gg(s(X), s(Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U5_agg(X, Y, geq_out_gg(X, Y)) → rem_out_agg(X, Y, X)
U3_agg(X, Y, R, rem_out_agg(Z, Y, R)) → rem_out_agg(X, Y, R)
U3_gag(X, Y, R, rem_out_agg(Z, Y, R)) → rem_out_gag(X, Y, R)
rem_in_gag(X, Y, X) → U4_gag(X, Y, notZero_in_a(Y))
U4_gag(X, Y, notZero_out_a(Y)) → U5_gag(X, Y, geq_in_gg(X, Y))
U5_gag(X, Y, geq_out_gg(X, Y)) → rem_out_gag(X, Y, X)
REM_IN_GAG(X, Y, R) → U1_GAG(X, Y, R, notZero_in_a(Y))
REM_IN_GAG(X, Y, R) → NOTZERO_IN_A(Y)
U1_GAG(X, Y, R, notZero_out_a(Y)) → U2_GAG(X, Y, R, sub_in_gga(X, Y, Z))
U1_GAG(X, Y, R, notZero_out_a(Y)) → SUB_IN_GGA(X, Y, Z)
SUB_IN_GGA(s(X), s(Y), Z) → U6_GGA(X, Y, Z, sub_in_aaa(X, Y, Z))
SUB_IN_GGA(s(X), s(Y), Z) → SUB_IN_AAA(X, Y, Z)
SUB_IN_AAA(s(X), s(Y), Z) → U6_AAA(X, Y, Z, sub_in_aaa(X, Y, Z))
SUB_IN_AAA(s(X), s(Y), Z) → SUB_IN_AAA(X, Y, Z)
U2_GAG(X, Y, R, sub_out_gga(X, Y, Z)) → U3_GAG(X, Y, R, rem_in_agg(Z, Y, R))
U2_GAG(X, Y, R, sub_out_gga(X, Y, Z)) → REM_IN_AGG(Z, Y, R)
REM_IN_AGG(X, Y, R) → U1_AGG(X, Y, R, notZero_in_g(Y))
REM_IN_AGG(X, Y, R) → NOTZERO_IN_G(Y)
U1_AGG(X, Y, R, notZero_out_g(Y)) → U2_AGG(X, Y, R, sub_in_aga(X, Y, Z))
U1_AGG(X, Y, R, notZero_out_g(Y)) → SUB_IN_AGA(X, Y, Z)
SUB_IN_AGA(s(X), s(Y), Z) → U6_AGA(X, Y, Z, sub_in_aaa(X, Y, Z))
SUB_IN_AGA(s(X), s(Y), Z) → SUB_IN_AAA(X, Y, Z)
U2_AGG(X, Y, R, sub_out_aga(X, Y, Z)) → U3_AGG(X, Y, R, rem_in_agg(Z, Y, R))
U2_AGG(X, Y, R, sub_out_aga(X, Y, Z)) → REM_IN_AGG(Z, Y, R)
REM_IN_AGG(X, Y, X) → U4_AGG(X, Y, notZero_in_g(Y))
REM_IN_AGG(X, Y, X) → NOTZERO_IN_G(Y)
U4_AGG(X, Y, notZero_out_g(Y)) → U5_AGG(X, Y, geq_in_gg(X, Y))
U4_AGG(X, Y, notZero_out_g(Y)) → GEQ_IN_GG(X, Y)
GEQ_IN_GG(s(X), s(Y)) → U7_GG(X, Y, geq_in_aa(X, Y))
GEQ_IN_GG(s(X), s(Y)) → GEQ_IN_AA(X, Y)
GEQ_IN_AA(s(X), s(Y)) → U7_AA(X, Y, geq_in_aa(X, Y))
GEQ_IN_AA(s(X), s(Y)) → GEQ_IN_AA(X, Y)
REM_IN_GAG(X, Y, X) → U4_GAG(X, Y, notZero_in_a(Y))
REM_IN_GAG(X, Y, X) → NOTZERO_IN_A(Y)
U4_GAG(X, Y, notZero_out_a(Y)) → U5_GAG(X, Y, geq_in_gg(X, Y))
U4_GAG(X, Y, notZero_out_a(Y)) → GEQ_IN_GG(X, Y)
rem_in_gag(X, Y, R) → U1_gag(X, Y, R, notZero_in_a(Y))
notZero_in_a(s(X)) → notZero_out_a(s(X))
U1_gag(X, Y, R, notZero_out_a(Y)) → U2_gag(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_aaa(X, Y, Z))
sub_in_aaa(s(X), s(Y), Z) → U6_aaa(X, Y, Z, sub_in_aaa(X, Y, Z))
sub_in_aaa(X, 0, X) → sub_out_aaa(X, 0, X)
U6_aaa(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_aaa(s(X), s(Y), Z)
U6_gga(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U2_gag(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gag(X, Y, R, rem_in_agg(Z, Y, R))
rem_in_agg(X, Y, R) → U1_agg(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_agg(X, Y, R, notZero_out_g(Y)) → U2_agg(X, Y, R, sub_in_aga(X, Y, Z))
sub_in_aga(s(X), s(Y), Z) → U6_aga(X, Y, Z, sub_in_aaa(X, Y, Z))
U6_aga(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_aga(s(X), s(Y), Z)
sub_in_aga(X, 0, X) → sub_out_aga(X, 0, X)
U2_agg(X, Y, R, sub_out_aga(X, Y, Z)) → U3_agg(X, Y, R, rem_in_agg(Z, Y, R))
rem_in_agg(X, Y, X) → U4_agg(X, Y, notZero_in_g(Y))
U4_agg(X, Y, notZero_out_g(Y)) → U5_agg(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_aa(X, Y))
geq_in_aa(s(X), s(Y)) → U7_aa(X, Y, geq_in_aa(X, Y))
geq_in_aa(X, 0) → geq_out_aa(X, 0)
U7_aa(X, Y, geq_out_aa(X, Y)) → geq_out_aa(s(X), s(Y))
U7_gg(X, Y, geq_out_aa(X, Y)) → geq_out_gg(s(X), s(Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U5_agg(X, Y, geq_out_gg(X, Y)) → rem_out_agg(X, Y, X)
U3_agg(X, Y, R, rem_out_agg(Z, Y, R)) → rem_out_agg(X, Y, R)
U3_gag(X, Y, R, rem_out_agg(Z, Y, R)) → rem_out_gag(X, Y, R)
rem_in_gag(X, Y, X) → U4_gag(X, Y, notZero_in_a(Y))
U4_gag(X, Y, notZero_out_a(Y)) → U5_gag(X, Y, geq_in_gg(X, Y))
U5_gag(X, Y, geq_out_gg(X, Y)) → rem_out_gag(X, Y, X)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
REM_IN_GAG(X, Y, R) → U1_GAG(X, Y, R, notZero_in_a(Y))
REM_IN_GAG(X, Y, R) → NOTZERO_IN_A(Y)
U1_GAG(X, Y, R, notZero_out_a(Y)) → U2_GAG(X, Y, R, sub_in_gga(X, Y, Z))
U1_GAG(X, Y, R, notZero_out_a(Y)) → SUB_IN_GGA(X, Y, Z)
SUB_IN_GGA(s(X), s(Y), Z) → U6_GGA(X, Y, Z, sub_in_aaa(X, Y, Z))
SUB_IN_GGA(s(X), s(Y), Z) → SUB_IN_AAA(X, Y, Z)
SUB_IN_AAA(s(X), s(Y), Z) → U6_AAA(X, Y, Z, sub_in_aaa(X, Y, Z))
SUB_IN_AAA(s(X), s(Y), Z) → SUB_IN_AAA(X, Y, Z)
U2_GAG(X, Y, R, sub_out_gga(X, Y, Z)) → U3_GAG(X, Y, R, rem_in_agg(Z, Y, R))
U2_GAG(X, Y, R, sub_out_gga(X, Y, Z)) → REM_IN_AGG(Z, Y, R)
REM_IN_AGG(X, Y, R) → U1_AGG(X, Y, R, notZero_in_g(Y))
REM_IN_AGG(X, Y, R) → NOTZERO_IN_G(Y)
U1_AGG(X, Y, R, notZero_out_g(Y)) → U2_AGG(X, Y, R, sub_in_aga(X, Y, Z))
U1_AGG(X, Y, R, notZero_out_g(Y)) → SUB_IN_AGA(X, Y, Z)
SUB_IN_AGA(s(X), s(Y), Z) → U6_AGA(X, Y, Z, sub_in_aaa(X, Y, Z))
SUB_IN_AGA(s(X), s(Y), Z) → SUB_IN_AAA(X, Y, Z)
U2_AGG(X, Y, R, sub_out_aga(X, Y, Z)) → U3_AGG(X, Y, R, rem_in_agg(Z, Y, R))
U2_AGG(X, Y, R, sub_out_aga(X, Y, Z)) → REM_IN_AGG(Z, Y, R)
REM_IN_AGG(X, Y, X) → U4_AGG(X, Y, notZero_in_g(Y))
REM_IN_AGG(X, Y, X) → NOTZERO_IN_G(Y)
U4_AGG(X, Y, notZero_out_g(Y)) → U5_AGG(X, Y, geq_in_gg(X, Y))
U4_AGG(X, Y, notZero_out_g(Y)) → GEQ_IN_GG(X, Y)
GEQ_IN_GG(s(X), s(Y)) → U7_GG(X, Y, geq_in_aa(X, Y))
GEQ_IN_GG(s(X), s(Y)) → GEQ_IN_AA(X, Y)
GEQ_IN_AA(s(X), s(Y)) → U7_AA(X, Y, geq_in_aa(X, Y))
GEQ_IN_AA(s(X), s(Y)) → GEQ_IN_AA(X, Y)
REM_IN_GAG(X, Y, X) → U4_GAG(X, Y, notZero_in_a(Y))
REM_IN_GAG(X, Y, X) → NOTZERO_IN_A(Y)
U4_GAG(X, Y, notZero_out_a(Y)) → U5_GAG(X, Y, geq_in_gg(X, Y))
U4_GAG(X, Y, notZero_out_a(Y)) → GEQ_IN_GG(X, Y)
rem_in_gag(X, Y, R) → U1_gag(X, Y, R, notZero_in_a(Y))
notZero_in_a(s(X)) → notZero_out_a(s(X))
U1_gag(X, Y, R, notZero_out_a(Y)) → U2_gag(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_aaa(X, Y, Z))
sub_in_aaa(s(X), s(Y), Z) → U6_aaa(X, Y, Z, sub_in_aaa(X, Y, Z))
sub_in_aaa(X, 0, X) → sub_out_aaa(X, 0, X)
U6_aaa(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_aaa(s(X), s(Y), Z)
U6_gga(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U2_gag(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gag(X, Y, R, rem_in_agg(Z, Y, R))
rem_in_agg(X, Y, R) → U1_agg(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_agg(X, Y, R, notZero_out_g(Y)) → U2_agg(X, Y, R, sub_in_aga(X, Y, Z))
sub_in_aga(s(X), s(Y), Z) → U6_aga(X, Y, Z, sub_in_aaa(X, Y, Z))
U6_aga(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_aga(s(X), s(Y), Z)
sub_in_aga(X, 0, X) → sub_out_aga(X, 0, X)
U2_agg(X, Y, R, sub_out_aga(X, Y, Z)) → U3_agg(X, Y, R, rem_in_agg(Z, Y, R))
rem_in_agg(X, Y, X) → U4_agg(X, Y, notZero_in_g(Y))
U4_agg(X, Y, notZero_out_g(Y)) → U5_agg(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_aa(X, Y))
geq_in_aa(s(X), s(Y)) → U7_aa(X, Y, geq_in_aa(X, Y))
geq_in_aa(X, 0) → geq_out_aa(X, 0)
U7_aa(X, Y, geq_out_aa(X, Y)) → geq_out_aa(s(X), s(Y))
U7_gg(X, Y, geq_out_aa(X, Y)) → geq_out_gg(s(X), s(Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U5_agg(X, Y, geq_out_gg(X, Y)) → rem_out_agg(X, Y, X)
U3_agg(X, Y, R, rem_out_agg(Z, Y, R)) → rem_out_agg(X, Y, R)
U3_gag(X, Y, R, rem_out_agg(Z, Y, R)) → rem_out_gag(X, Y, R)
rem_in_gag(X, Y, X) → U4_gag(X, Y, notZero_in_a(Y))
U4_gag(X, Y, notZero_out_a(Y)) → U5_gag(X, Y, geq_in_gg(X, Y))
U5_gag(X, Y, geq_out_gg(X, Y)) → rem_out_gag(X, Y, X)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDP
GEQ_IN_AA(s(X), s(Y)) → GEQ_IN_AA(X, Y)
rem_in_gag(X, Y, R) → U1_gag(X, Y, R, notZero_in_a(Y))
notZero_in_a(s(X)) → notZero_out_a(s(X))
U1_gag(X, Y, R, notZero_out_a(Y)) → U2_gag(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_aaa(X, Y, Z))
sub_in_aaa(s(X), s(Y), Z) → U6_aaa(X, Y, Z, sub_in_aaa(X, Y, Z))
sub_in_aaa(X, 0, X) → sub_out_aaa(X, 0, X)
U6_aaa(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_aaa(s(X), s(Y), Z)
U6_gga(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U2_gag(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gag(X, Y, R, rem_in_agg(Z, Y, R))
rem_in_agg(X, Y, R) → U1_agg(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_agg(X, Y, R, notZero_out_g(Y)) → U2_agg(X, Y, R, sub_in_aga(X, Y, Z))
sub_in_aga(s(X), s(Y), Z) → U6_aga(X, Y, Z, sub_in_aaa(X, Y, Z))
U6_aga(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_aga(s(X), s(Y), Z)
sub_in_aga(X, 0, X) → sub_out_aga(X, 0, X)
U2_agg(X, Y, R, sub_out_aga(X, Y, Z)) → U3_agg(X, Y, R, rem_in_agg(Z, Y, R))
rem_in_agg(X, Y, X) → U4_agg(X, Y, notZero_in_g(Y))
U4_agg(X, Y, notZero_out_g(Y)) → U5_agg(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_aa(X, Y))
geq_in_aa(s(X), s(Y)) → U7_aa(X, Y, geq_in_aa(X, Y))
geq_in_aa(X, 0) → geq_out_aa(X, 0)
U7_aa(X, Y, geq_out_aa(X, Y)) → geq_out_aa(s(X), s(Y))
U7_gg(X, Y, geq_out_aa(X, Y)) → geq_out_gg(s(X), s(Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U5_agg(X, Y, geq_out_gg(X, Y)) → rem_out_agg(X, Y, X)
U3_agg(X, Y, R, rem_out_agg(Z, Y, R)) → rem_out_agg(X, Y, R)
U3_gag(X, Y, R, rem_out_agg(Z, Y, R)) → rem_out_gag(X, Y, R)
rem_in_gag(X, Y, X) → U4_gag(X, Y, notZero_in_a(Y))
U4_gag(X, Y, notZero_out_a(Y)) → U5_gag(X, Y, geq_in_gg(X, Y))
U5_gag(X, Y, geq_out_gg(X, Y)) → rem_out_gag(X, Y, X)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PiDP
GEQ_IN_AA(s(X), s(Y)) → GEQ_IN_AA(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ NonTerminationProof
↳ PiDP
↳ PiDP
GEQ_IN_AA → GEQ_IN_AA
GEQ_IN_AA → GEQ_IN_AA
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
SUB_IN_AAA(s(X), s(Y), Z) → SUB_IN_AAA(X, Y, Z)
rem_in_gag(X, Y, R) → U1_gag(X, Y, R, notZero_in_a(Y))
notZero_in_a(s(X)) → notZero_out_a(s(X))
U1_gag(X, Y, R, notZero_out_a(Y)) → U2_gag(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_aaa(X, Y, Z))
sub_in_aaa(s(X), s(Y), Z) → U6_aaa(X, Y, Z, sub_in_aaa(X, Y, Z))
sub_in_aaa(X, 0, X) → sub_out_aaa(X, 0, X)
U6_aaa(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_aaa(s(X), s(Y), Z)
U6_gga(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U2_gag(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gag(X, Y, R, rem_in_agg(Z, Y, R))
rem_in_agg(X, Y, R) → U1_agg(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_agg(X, Y, R, notZero_out_g(Y)) → U2_agg(X, Y, R, sub_in_aga(X, Y, Z))
sub_in_aga(s(X), s(Y), Z) → U6_aga(X, Y, Z, sub_in_aaa(X, Y, Z))
U6_aga(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_aga(s(X), s(Y), Z)
sub_in_aga(X, 0, X) → sub_out_aga(X, 0, X)
U2_agg(X, Y, R, sub_out_aga(X, Y, Z)) → U3_agg(X, Y, R, rem_in_agg(Z, Y, R))
rem_in_agg(X, Y, X) → U4_agg(X, Y, notZero_in_g(Y))
U4_agg(X, Y, notZero_out_g(Y)) → U5_agg(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_aa(X, Y))
geq_in_aa(s(X), s(Y)) → U7_aa(X, Y, geq_in_aa(X, Y))
geq_in_aa(X, 0) → geq_out_aa(X, 0)
U7_aa(X, Y, geq_out_aa(X, Y)) → geq_out_aa(s(X), s(Y))
U7_gg(X, Y, geq_out_aa(X, Y)) → geq_out_gg(s(X), s(Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U5_agg(X, Y, geq_out_gg(X, Y)) → rem_out_agg(X, Y, X)
U3_agg(X, Y, R, rem_out_agg(Z, Y, R)) → rem_out_agg(X, Y, R)
U3_gag(X, Y, R, rem_out_agg(Z, Y, R)) → rem_out_gag(X, Y, R)
rem_in_gag(X, Y, X) → U4_gag(X, Y, notZero_in_a(Y))
U4_gag(X, Y, notZero_out_a(Y)) → U5_gag(X, Y, geq_in_gg(X, Y))
U5_gag(X, Y, geq_out_gg(X, Y)) → rem_out_gag(X, Y, X)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
SUB_IN_AAA(s(X), s(Y), Z) → SUB_IN_AAA(X, Y, Z)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ NonTerminationProof
↳ PiDP
SUB_IN_AAA → SUB_IN_AAA
SUB_IN_AAA → SUB_IN_AAA
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
U1_AGG(X, Y, R, notZero_out_g(Y)) → U2_AGG(X, Y, R, sub_in_aga(X, Y, Z))
U2_AGG(X, Y, R, sub_out_aga(X, Y, Z)) → REM_IN_AGG(Z, Y, R)
REM_IN_AGG(X, Y, R) → U1_AGG(X, Y, R, notZero_in_g(Y))
rem_in_gag(X, Y, R) → U1_gag(X, Y, R, notZero_in_a(Y))
notZero_in_a(s(X)) → notZero_out_a(s(X))
U1_gag(X, Y, R, notZero_out_a(Y)) → U2_gag(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_aaa(X, Y, Z))
sub_in_aaa(s(X), s(Y), Z) → U6_aaa(X, Y, Z, sub_in_aaa(X, Y, Z))
sub_in_aaa(X, 0, X) → sub_out_aaa(X, 0, X)
U6_aaa(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_aaa(s(X), s(Y), Z)
U6_gga(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U2_gag(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gag(X, Y, R, rem_in_agg(Z, Y, R))
rem_in_agg(X, Y, R) → U1_agg(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_agg(X, Y, R, notZero_out_g(Y)) → U2_agg(X, Y, R, sub_in_aga(X, Y, Z))
sub_in_aga(s(X), s(Y), Z) → U6_aga(X, Y, Z, sub_in_aaa(X, Y, Z))
U6_aga(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_aga(s(X), s(Y), Z)
sub_in_aga(X, 0, X) → sub_out_aga(X, 0, X)
U2_agg(X, Y, R, sub_out_aga(X, Y, Z)) → U3_agg(X, Y, R, rem_in_agg(Z, Y, R))
rem_in_agg(X, Y, X) → U4_agg(X, Y, notZero_in_g(Y))
U4_agg(X, Y, notZero_out_g(Y)) → U5_agg(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_aa(X, Y))
geq_in_aa(s(X), s(Y)) → U7_aa(X, Y, geq_in_aa(X, Y))
geq_in_aa(X, 0) → geq_out_aa(X, 0)
U7_aa(X, Y, geq_out_aa(X, Y)) → geq_out_aa(s(X), s(Y))
U7_gg(X, Y, geq_out_aa(X, Y)) → geq_out_gg(s(X), s(Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U5_agg(X, Y, geq_out_gg(X, Y)) → rem_out_agg(X, Y, X)
U3_agg(X, Y, R, rem_out_agg(Z, Y, R)) → rem_out_agg(X, Y, R)
U3_gag(X, Y, R, rem_out_agg(Z, Y, R)) → rem_out_gag(X, Y, R)
rem_in_gag(X, Y, X) → U4_gag(X, Y, notZero_in_a(Y))
U4_gag(X, Y, notZero_out_a(Y)) → U5_gag(X, Y, geq_in_gg(X, Y))
U5_gag(X, Y, geq_out_gg(X, Y)) → rem_out_gag(X, Y, X)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
U1_AGG(X, Y, R, notZero_out_g(Y)) → U2_AGG(X, Y, R, sub_in_aga(X, Y, Z))
U2_AGG(X, Y, R, sub_out_aga(X, Y, Z)) → REM_IN_AGG(Z, Y, R)
REM_IN_AGG(X, Y, R) → U1_AGG(X, Y, R, notZero_in_g(Y))
sub_in_aga(s(X), s(Y), Z) → U6_aga(X, Y, Z, sub_in_aaa(X, Y, Z))
sub_in_aga(X, 0, X) → sub_out_aga(X, 0, X)
notZero_in_g(s(X)) → notZero_out_g(s(X))
U6_aga(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_aga(s(X), s(Y), Z)
sub_in_aaa(s(X), s(Y), Z) → U6_aaa(X, Y, Z, sub_in_aaa(X, Y, Z))
sub_in_aaa(X, 0, X) → sub_out_aaa(X, 0, X)
U6_aaa(X, Y, Z, sub_out_aaa(X, Y, Z)) → sub_out_aaa(s(X), s(Y), Z)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
U1_AGG(Y, R, notZero_out_g(Y)) → U2_AGG(Y, R, sub_in_aga(Y))
REM_IN_AGG(Y, R) → U1_AGG(Y, R, notZero_in_g(Y))
U2_AGG(Y, R, sub_out_aga(Y)) → REM_IN_AGG(Y, R)
sub_in_aga(s) → U6_aga(sub_in_aaa)
sub_in_aga(0) → sub_out_aga(0)
notZero_in_g(s) → notZero_out_g(s)
U6_aga(sub_out_aaa(Y)) → sub_out_aga(s)
sub_in_aaa → U6_aaa(sub_in_aaa)
sub_in_aaa → sub_out_aaa(0)
U6_aaa(sub_out_aaa(Y)) → sub_out_aaa(s)
sub_in_aga(x0)
notZero_in_g(x0)
U6_aga(x0)
sub_in_aaa
U6_aaa(x0)
U1_AGG(0, y1, notZero_out_g(0)) → U2_AGG(0, y1, sub_out_aga(0))
U1_AGG(s, y1, notZero_out_g(s)) → U2_AGG(s, y1, U6_aga(sub_in_aaa))
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
U1_AGG(s, y1, notZero_out_g(s)) → U2_AGG(s, y1, U6_aga(sub_in_aaa))
U1_AGG(0, y1, notZero_out_g(0)) → U2_AGG(0, y1, sub_out_aga(0))
REM_IN_AGG(Y, R) → U1_AGG(Y, R, notZero_in_g(Y))
U2_AGG(Y, R, sub_out_aga(Y)) → REM_IN_AGG(Y, R)
sub_in_aga(s) → U6_aga(sub_in_aaa)
sub_in_aga(0) → sub_out_aga(0)
notZero_in_g(s) → notZero_out_g(s)
U6_aga(sub_out_aaa(Y)) → sub_out_aga(s)
sub_in_aaa → U6_aaa(sub_in_aaa)
sub_in_aaa → sub_out_aaa(0)
U6_aaa(sub_out_aaa(Y)) → sub_out_aaa(s)
sub_in_aga(x0)
notZero_in_g(x0)
U6_aga(x0)
sub_in_aaa
U6_aaa(x0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
U1_AGG(s, y1, notZero_out_g(s)) → U2_AGG(s, y1, U6_aga(sub_in_aaa))
REM_IN_AGG(Y, R) → U1_AGG(Y, R, notZero_in_g(Y))
U2_AGG(Y, R, sub_out_aga(Y)) → REM_IN_AGG(Y, R)
sub_in_aga(s) → U6_aga(sub_in_aaa)
sub_in_aga(0) → sub_out_aga(0)
notZero_in_g(s) → notZero_out_g(s)
U6_aga(sub_out_aaa(Y)) → sub_out_aga(s)
sub_in_aaa → U6_aaa(sub_in_aaa)
sub_in_aaa → sub_out_aaa(0)
U6_aaa(sub_out_aaa(Y)) → sub_out_aaa(s)
sub_in_aga(x0)
notZero_in_g(x0)
U6_aga(x0)
sub_in_aaa
U6_aaa(x0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
U1_AGG(s, y1, notZero_out_g(s)) → U2_AGG(s, y1, U6_aga(sub_in_aaa))
REM_IN_AGG(Y, R) → U1_AGG(Y, R, notZero_in_g(Y))
U2_AGG(Y, R, sub_out_aga(Y)) → REM_IN_AGG(Y, R)
sub_in_aaa → U6_aaa(sub_in_aaa)
sub_in_aaa → sub_out_aaa(0)
U6_aga(sub_out_aaa(Y)) → sub_out_aga(s)
U6_aaa(sub_out_aaa(Y)) → sub_out_aaa(s)
notZero_in_g(s) → notZero_out_g(s)
sub_in_aga(x0)
notZero_in_g(x0)
U6_aga(x0)
sub_in_aaa
U6_aaa(x0)
sub_in_aga(x0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
REM_IN_AGG(Y, R) → U1_AGG(Y, R, notZero_in_g(Y))
U1_AGG(s, y1, notZero_out_g(s)) → U2_AGG(s, y1, U6_aga(sub_in_aaa))
U2_AGG(Y, R, sub_out_aga(Y)) → REM_IN_AGG(Y, R)
sub_in_aaa → U6_aaa(sub_in_aaa)
sub_in_aaa → sub_out_aaa(0)
U6_aga(sub_out_aaa(Y)) → sub_out_aga(s)
U6_aaa(sub_out_aaa(Y)) → sub_out_aaa(s)
notZero_in_g(s) → notZero_out_g(s)
notZero_in_g(x0)
U6_aga(x0)
sub_in_aaa
U6_aaa(x0)
REM_IN_AGG(s, y1) → U1_AGG(s, y1, notZero_out_g(s))
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
REM_IN_AGG(s, y1) → U1_AGG(s, y1, notZero_out_g(s))
U1_AGG(s, y1, notZero_out_g(s)) → U2_AGG(s, y1, U6_aga(sub_in_aaa))
U2_AGG(Y, R, sub_out_aga(Y)) → REM_IN_AGG(Y, R)
sub_in_aaa → U6_aaa(sub_in_aaa)
sub_in_aaa → sub_out_aaa(0)
U6_aga(sub_out_aaa(Y)) → sub_out_aga(s)
U6_aaa(sub_out_aaa(Y)) → sub_out_aaa(s)
notZero_in_g(s) → notZero_out_g(s)
notZero_in_g(x0)
U6_aga(x0)
sub_in_aaa
U6_aaa(x0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
REM_IN_AGG(s, y1) → U1_AGG(s, y1, notZero_out_g(s))
U1_AGG(s, y1, notZero_out_g(s)) → U2_AGG(s, y1, U6_aga(sub_in_aaa))
U2_AGG(Y, R, sub_out_aga(Y)) → REM_IN_AGG(Y, R)
sub_in_aaa → U6_aaa(sub_in_aaa)
sub_in_aaa → sub_out_aaa(0)
U6_aga(sub_out_aaa(Y)) → sub_out_aga(s)
U6_aaa(sub_out_aaa(Y)) → sub_out_aaa(s)
notZero_in_g(x0)
U6_aga(x0)
sub_in_aaa
U6_aaa(x0)
notZero_in_g(x0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
REM_IN_AGG(s, y1) → U1_AGG(s, y1, notZero_out_g(s))
U1_AGG(s, y1, notZero_out_g(s)) → U2_AGG(s, y1, U6_aga(sub_in_aaa))
U2_AGG(Y, R, sub_out_aga(Y)) → REM_IN_AGG(Y, R)
sub_in_aaa → U6_aaa(sub_in_aaa)
sub_in_aaa → sub_out_aaa(0)
U6_aga(sub_out_aaa(Y)) → sub_out_aga(s)
U6_aaa(sub_out_aaa(Y)) → sub_out_aaa(s)
U6_aga(x0)
sub_in_aaa
U6_aaa(x0)
U2_AGG(s, z0, sub_out_aga(s)) → REM_IN_AGG(s, z0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ NonTerminationProof
REM_IN_AGG(s, y1) → U1_AGG(s, y1, notZero_out_g(s))
U2_AGG(s, z0, sub_out_aga(s)) → REM_IN_AGG(s, z0)
U1_AGG(s, y1, notZero_out_g(s)) → U2_AGG(s, y1, U6_aga(sub_in_aaa))
sub_in_aaa → U6_aaa(sub_in_aaa)
sub_in_aaa → sub_out_aaa(0)
U6_aga(sub_out_aaa(Y)) → sub_out_aga(s)
U6_aaa(sub_out_aaa(Y)) → sub_out_aaa(s)
U6_aga(x0)
sub_in_aaa
U6_aaa(x0)
REM_IN_AGG(s, y1) → U1_AGG(s, y1, notZero_out_g(s))
U2_AGG(s, z0, sub_out_aga(s)) → REM_IN_AGG(s, z0)
U1_AGG(s, y1, notZero_out_g(s)) → U2_AGG(s, y1, U6_aga(sub_in_aaa))
sub_in_aaa → U6_aaa(sub_in_aaa)
sub_in_aaa → sub_out_aaa(0)
U6_aga(sub_out_aaa(Y)) → sub_out_aga(s)
U6_aaa(sub_out_aaa(Y)) → sub_out_aaa(s)